Avail - Library

random access buffered iterator, natural number

Source: /avail/Avail/Data Abstractions/Iterators/Random Access Buffered Iterators

Set the current position of the random access buffered iterator.

	Position	Name	Type	Description
Parameters
	1	anIterator	random access buffered iterator	A random access buffered iterator.
	2	position	natural number	A position memento that represents a valid position.
Returns			⊤
Raises
Raises			invalid-position exception	If position is not a valid memento.

positionable iterator, any

Source: /avail/Avail/Data Abstractions/Iterators/Positionable Iterators

Set the current position of the positionable iterator.

	Position	Name	Type	Description
Parameters
	1	anIterator	positionable iterator	A positionable iterator.
	2	position	any	A position memento that represents a valid position.
Returns			⊤
Raises
Raises			invalid-position exception	If position is not a valid memento.

positionable iterator's type's type, any's type

Source: /avail/Avail/Data Abstractions/Iterators/Positionable Iterators

Ensure the new position is suitable.

	Type	Description
Parameter Types
	positionable iterator's type's type
	any's type

anIterator, position

Source: /avail/Avail/Data Abstractions/Iterators/Collection Readers

Reject the positioning attempt statically if it's known that the new position is always out of bounds.

_'s⁇position:=_